Inference at * 1 
Iof proof for Lemma fun with inv is bij:



1. A : Type
2. B : Type
3. f : AB
4. g : BA
5. InvFuns(A;B;f;g)
  Bij(A;B;f) 

latex

 by D 5 

latex

 1: 

 1: 5. (g o f) = Id{A}
 1: 6. (f o g) = Id{B}
 1:   Bij(A;B;f)
 .

Definitions

P & Q, InvFuns(A;B;f;g)